import 'http://www.istr.unican.es/CVS'

package cvs

-- ------------------------
-- Constraints on CVS_Model
-- ------------------------
					  
-- Every NON-INSTANTIABLE SimpleCategory must be used by at least one ComplexCategory
context CVS_Model
	inv i_1:
		categories -> select(c | c.oclIsTypeOf(SimpleCategory)) -> 
		              select(sc | sc.oclAsType(SimpleCategory).instantiable = false) -> 
		              forAll(nisc | ComplexCategory.allInstances() -> exists(cc | cc.instantiations -> exists(i | i.category = nisc)))


		              


-- -----------------------------------
-- Constraints on ObjectsSpecification
-- -----------------------------------

-- The referenced Category must be an INSTANTIABLE SimpleCategory or a ComplexCategory
context ObjectsSpecification
	inv i_4:
		category.oclIsTypeOf(ComplexCategory) or 
		(category.oclIsTypeOf(SimpleCategory) and category.oclAsType(SimpleCategory).instantiable = true)



-- -----------------------------
-- Constraints on SimpleCategory
-- -----------------------------

-- The referenced base EClass must be concrete
context SimpleCategory
	inv i_5: 
		srcClass.abstract = false

-- For every contained AttrImposition, the EAttribute referenced through srcAttr must belong to the base EClass
context SimpleCategory
	inv i_6:
		attrImpositions -> forAll(ai | srcClass.eAllAttributes -> includes(ai.srcAttr))

-- For every contained EqualizationWithOtherAttr, the EAttribute referenced by otherAttr must belong to the base EClass
context SimpleCategory
	inv i_7:
		attrImpositions -> select(ai | ai.oclIsTypeOf(EqualizationWithOtherAttr)) -> 
		                   forAll(ai | srcClass.eAllAttributes -> includes(ai.oclAsType(EqualizationWithOtherAttr).otherAttr))

-- Different AttrImpositions must point to different EAttributes
context SimpleCategory
	inv i_8:
		attrImpositions -> forAll(ai1, ai2 | ai1 <> ai2 implies ai1.srcAttr <> ai2.srcAttr)

-- For every contained RefImposition, the EReference referenced through srcRef must belong to the base EClass
context SimpleCategory
	inv i_9:
		refImpositions -> forAll(ri | srcClass.eAllReferences -> includes(ri.srcRef))

-- For every contained EqualizationWithOtherRef, the EReference referenced through otherRef must belong to the base EClass
context SimpleCategory
	inv i_10:
		refImpositions -> select(ri | ri.oclIsTypeOf(EqualizationWithOtherRef)) -> 
		                  forAll(ri | srcClass.eAllReferences -> includes(ri.oclAsType(EqualizationWithOtherRef).otherRef))

-- Different RefImpositions must point to different EReferences
context SimpleCategory
	inv i_11:
		refImpositions -> forAll(ri1, ri2 | ri1 <> ri2 implies ri1.srcRef <> ri2.srcRef)

-- It must contain one RefImposition for every EReference of the base EClass 
context SimpleCategory
	inv i_12:
		srcClass.eAllReferences -> forAll(er | refImpositions -> exists(ri | ri.srcRef = er))




-- --------------------------------
-- Constraints on TypeSpecification
-- --------------------------------

--
--context TypingSpecification
--	inv i_:




-- ------------------------------------
-- Constraints on CategoryInstantiation
-- ------------------------------------

-- For every contained RefAssignment, the EReference pointed through assignedRef must belong to the base EClass on which the instantiated category has been defined.
context CategoryInstantiation
	inv i_2s:
		refAssignments -> forAll(ra | category.oclAsType(SimpleCategory).srcClass.eAllReferences -> includes(ra.assignedRef))

-- 
--context CategoryInstantiation
--	inv i_2s:



endpackage